COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(defun alt (u) (cond ((or (null u) (null (cdr u))) u)
C00005 ENDMK
C⊗;
(defun alt (u) (cond ((or (null u) (null (cdr u))) u)
		     (t (cons (car u) (alt (cddr u))))))
(A C E) 
(alt '(a b c d e))
(proof cycle)
(dskin cycle)
NIL 
NIL 
NIL 
NIL 
NIL 
NIL 
NIL 8. ∀G.ATOM(G)⊃SEXP(G)
   ctxt: (1 2 4)   deps: NIL

NIL 9. ∀X Y.SEXP(CONS(X,Y))
   ctxt: (1 6)   deps: NIL

NIL 10. ∀G.SEXP(G)⊃ATOM(G)∨(∃X Y.G=CONS(X,Y))
    ctxt: (1 2 4 6)   deps: NIL

NIL 11. ∀X Y.¬ATOM(CONS(X,Y))
    ctxt: (1 2 6)   deps: NIL

NIL 12. ∀X Y.CAR(CONS(X,Y))=X
    ctxt: (1 5 6)   deps: NIL

NIL 13. ∀X Y.CDR(CONS(X,Y))=Y
    ctxt: (1 5 6)   deps: NIL

NIL 14. ∀PHI A.PHI(A)∧(∀X Y.(PHI(X)∧PHI(Y)⊃PHI(CONS(X,Y)))⊃(∀X.PHI(X)))
    ctxt: (1 2 6 7)   deps: NIL

NIL 
NIL 
NIL 17. NULL(NNIL)
    ctxt: (3 16)   deps: NIL

NIL 18. ∀U.NULL(U)≡U=NNIL
    ctxt: (3 15 16)   deps: NIL

NIL 19. LIST(NNIL)
    ctxt: (3 15)   deps: NIL

NIL 20. ∀G.LIST(G)⊃SEXP(G)
    ctxt: (1 4 15)   deps: NIL

NIL 21. ∀X U.¬NULL(CONS(X,U))
    ctxt: (1 6 15 16)   deps: NIL

NIL 
CYCLE done.
* the symbol RDC is unknown - declared to have type ?VTYP1
22. ∀X U.RDC(X,U)=IF NULL(U) THEN NNIL ELSE CONS(X,RDC(CAR(U),CDR(U)))
    ctxt: (1 3 5 6 15 16 22)   deps: NIL

* done.
*